\begin{tabbing}
(\=InductionOnNat) \+
\\[0ex]CollapseTHEN ((Reduce 0) 
\\[0ex]CollapseTHEN (((D (0)$\cdot$) 
\\[0ex]CollapseTHENA (
\-\\[0ex]A\=uto$\cdot$)$\cdot$) \+
\\[0ex]CollapseTHEN (((Try ((Complete ((ProveSqEq) 
\\[0ex]CollapseTHEN (Auto$\cdot$)$\cdot$))$\cdot$))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN ((RW (SubC (RecUnfoldTopC `primrec`)) 0) 
\\[0ex]CollapseTHEN (((if (((first\_nat 
\-\\[0ex]2\=:n)) = 0) then (Repeat ((((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0))$\cdot$) \+
\\[0ex]
\\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$) 
\\[0ex]CollapseTHEN ((Try ((Complete (Auto'))$\cdot$))$\cdot$)$\cdot$
\-\\[0ex])) else (RepeatFor (first\_nat 2:n) ((((if (0) =0 then SplitOnConclITE else SplitOnHypITE (
\\[0ex]0\=))$\cdot$) \+
\\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$) 
\\[0ex]CollapseTHEN ((Try ((Complete (Auto'))$\cdot$))$\cdot$)$\cdot$)))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN ((EqCD) 
\\[0ex]CollapseTHEN ((Reduce 0) 
\\[0ex]CollapseTHEN (((Try (Trivial))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN ((Subst' (($n$+$m$) {-} 1) $\sim$ (($n$ {-} 1)+$m$) ( 0)$\cdot$) 
\\[0ex]CollapseTHEN (((Try ((if ((0
\-\\[0ex])\= = 0) then BackThruSomeHyp else BHyp (0) )$\cdot$))$\cdot$) \+
\\[0ex]CollapseTHEN (Auto$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\-\\[0ex])$\cdot$
\end{tabbing}